Termination of the given ITRSProblem could not be shown:



↳ ITRS

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

Cond_eval1(TRUE, x, y) → eval(x, -@z(y, 1@z))
Cond_eval(TRUE, x, y, z) → eval(-@z(x, 1@z), z)
eval(x, y) → Cond_eval1(>=@z(y, 0@z), x, y)
eval(x, y) → Cond_eval(>=@z(x, 0@z), x, y, z)

The set Q consists of the following terms:

Cond_eval1(TRUE, x0, x1)
Cond_eval(TRUE, x0, x1, x2)
eval(x0, x1)